(set-logic QF_BV)
(declare-fun _substvar_3039_ () Bool)
(declare-fun _substvar_3209_ () Bool)
(declare-fun _substvar_2884_ () Bool)
(declare-fun _substvar_3237_ () Bool)
(declare-fun _substvar_83_ () (_ BitVec 4))
(declare-fun _substvar_35_ () (_ BitVec 4))
(declare-fun _substvar_3199_ () Bool)
(declare-fun _substvar_3142_ () Bool)
(declare-fun _substvar_81_ () (_ BitVec 4))
(declare-fun _substvar_100_ () (_ BitVec 4))
(declare-fun _substvar_80_ () (_ BitVec 4))
(assert (let ((.def_446 (= _substvar_35_ _substvar_80_))) (let ((.def_440 (= _substvar_80_ _substvar_81_))) (let ((.def_441 .def_440)) (let ((.def_444 .def_441)) (let ((.def_430 (= _substvar_81_ _substvar_83_))) (let ((.def_431 (or _substvar_3039_ .def_430))) (let ((.def_428 (bvxor _substvar_83_ _substvar_100_))) (let ((.def_429 (= _substvar_81_ .def_428))) (let ((.def_432 (not _substvar_3039_))) (let ((.def_433 (or .def_432 .def_429))) (let ((.def_434 (and .def_433 .def_431))) (let ((.def_420 (= _substvar_83_ (_ bv0 4)))) (let ((.def_421 .def_420)) (let ((.def_424 (and _substvar_2884_ .def_421))) (let ((.def_398 (= _substvar_100_ (_ bv0 4)))) (let ((.def_402 .def_398)) (let ((.def_403 .def_402)) (let ((.def_447 (= _substvar_35_ (_ bv0 4)))) (let ((.def_448 (not .def_447))) (let ((.def_449 .def_448)) (let ((.def_450 (and .def_449 _substvar_3209_))) (let ((.def_451 .def_450)) (let ((.def_452 .def_451)) (let ((.def_453 .def_452)) (let ((.def_454 .def_453)) (let ((.def_455 .def_454)) (let ((.def_456 .def_455)) (let ((.def_457 .def_456)) (let ((.def_458 .def_457)) (let ((.def_459 .def_458)) (let ((.def_460 .def_459)) (let ((.def_461 .def_460)) (let ((.def_462 .def_461)) (let ((.def_463 .def_462)) (let ((.def_464 .def_463)) (let ((.def_465 .def_464)) (let ((.def_466 .def_465)) (let ((.def_467 .def_466)) (let ((.def_468 .def_467)) (let ((.def_469 .def_468)) (let ((.def_470 .def_469)) (let ((.def_471 .def_470)) (let ((.def_472 .def_471)) (let ((.def_473 .def_472)) (let ((.def_474 .def_473)) (let ((.def_475 .def_474)) (let ((.def_476 .def_475)) (let ((.def_477 .def_476)) (let ((.def_478 .def_477)) (let ((.def_479 .def_478)) (let ((.def_480 .def_479)) (let ((.def_481 .def_480)) (let ((.def_482 .def_481)) (let ((.def_483 .def_482)) (let ((.def_484 .def_483)) (let ((.def_485 .def_484)) (let ((.def_486 .def_485)) (let ((.def_487 .def_486)) (let ((.def_488 .def_487)) (let ((.def_489 .def_488)) (let ((.def_490 .def_489)) (let ((.def_491 .def_490)) (let ((.def_492 .def_491)) (let ((.def_493 .def_492)) (let ((.def_494 .def_493)) (let ((.def_495 (and .def_494 _substvar_3142_))) (let ((.def_496 (and .def_495 _substvar_3237_))) (let ((.def_497 (and .def_496 _substvar_3199_))) (let ((.def_498 .def_497)) (let ((.def_499 (and .def_498 .def_403))) (let ((.def_500 .def_499)) (let ((.def_501 (and .def_500 .def_424))) (let ((.def_502 (and .def_501 .def_434))) (let ((.def_503 (and .def_502 .def_444))) (let ((.def_504 (and .def_503 .def_446))) .def_504))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
